
; Copyright (c) 2015 Microsoft Corporation

(set-option :print-success false)
(set-option :produce-models true)
(set-option :smt.mbqi true)
(set-option :print-warning false)

(define-sort double () Real)
(define-sort int32 () Int)
(define-sort boolean () Bool)

(declare-fun PRC_Pressure__controller_u_AT_out () double)
(declare-fun PRC_u_PA_in_0_ () double)
(declare-fun Controller.p_max () double)
(declare-fun PRC_u_PA_outMY_ABS_0_ () double)
(declare-fun PRC_p_A_1_ () double)
(declare-fun PRC_u_AT_in_y1_1_ () double)
(declare-fun PRC_p_AMY_ABS_0_ () double)
(declare-fun PRC_Rate__Transition__Out_y1 () double)
(declare-fun PRC_u_AT_outMY_ABS_1_ () double)
(declare-fun PRC_p_A () double)
(declare-fun PRC_u_AT_in () double)
(declare-fun PRC_u_AT_in_y1_0_ () double)
(declare-fun PRC_u_AT_outRTI_y1_1_ () double)
(declare-fun PRC_Filtering__of__pressure_in_d2_0_ () double)
(declare-fun PRC_p_A_y1 () double)
(declare-fun PRC_u_AT_inMY_ABS_0_ () double)
(declare-fun PRC_u_PA_inRTI_y1 () double)
(declare-fun PRC_u_PA_in_1_ () double)
(declare-fun PRC_in_d2_0_ () double)
(declare-fun PRC_u_PA_outMY_ABS_1_ () double)
(declare-fun PRC_u_PA_in_y1_0_ () double)
(declare-fun PRC_p_A_0_ () double)
(declare-fun PRC_u_AT_outMY_ABS_0_ () double)
(declare-fun PRC_Filtering__of__pressure_p_A_filtered_1_ () double)
(declare-fun PRC_Filtering__of__pressure_in_d1_1_ () double)
(declare-fun PRC_Filtering__of__pressure_in_d2_1_ () double)
(declare-fun PRC_u_PA_outRTI_y1_1_ () double)
(declare-fun PRC_u_AT_inRTI_y1 () double)
(declare-fun p_cracking () double)
(declare-fun PRC_in_d2_1_ () double)
(declare-fun PRC_u_PA_outRTI_y1_0_ () double)
(declare-fun PRC_Filtering__of__pressure_p_A_filtered_0_ () double)
(declare-fun Controller.p_hyst () double)
(declare-fun PRC_Filtering__of__pressure_in_d1_0_ () double)
(declare-fun PRC_in_d1_1_ () double)
(declare-fun PRC_u_AT_out_1_ () double)
(declare-fun PRC_u_PA_in () double)
(declare-fun PRC_u_AT_in_0_ () double)
(declare-fun PRC_u_PA_out_0_ () double)
(declare-fun PRC_u_PA_out () double)
(declare-fun PRC_u_AT_out () double)
(declare-fun PRC_Rate__Transition_X_1_ () double)
(declare-fun Controller.Q_max_unit () double)
(declare-fun Controller.pcCount () double)
(declare-fun PRC_u_PA_in_y1_1_ () double)
(declare-fun PRC_in_d1_0_ () double)
(declare-fun PRC_u_AT_out_0_ () double)
(declare-fun PRC_u_AT_outRTI_y1_0_ () double)
(declare-fun PRC_p_AMY_ABS_1_ () double)
(declare-fun PRC_u_AT_in_1_ () double)
(declare-fun PRC_Rate__Transition_X_0_ () double)
(declare-fun PRC_u_AT_inMY_ABS_1_ () double)
(declare-fun PRC_u_PA_out_1_ () double)
(declare-fun isinteger (double) boolean)
(declare-fun my_abs (double) double)
(declare-fun _NaN () double)
(declare-fun Inf () double)

(assert
(and (= Controller.p_hyst 5.0) (and (= Controller.Q_max_unit 1.5) (and (> Controller.Q_max_unit 0.0) (and (= Controller.pcCount 31.0) (and (isinteger Controller.pcCount ) (and (> Controller.pcCount 0.0) (and (= Controller.pcCount 31.0) (and (= Controller.p_max 200000.0) (and (= p_cracking (* 0.9 200000.0)) (< p_cracking Controller.p_max)))))))))))
(assert
(and (isinteger PRC_u_AT_in ) (and (> PRC_p_A (- 1000000.0)) (and (< PRC_p_A 1000000.0) (and (>= PRC_u_AT_in 0.0) (<= PRC_u_AT_in Controller.pcCount))))))
(assert
(and (and (and (and (and (and (and (= PRC_u_AT_out_1_ PRC_u_AT_outMY_ABS_1_) (= PRC_u_AT_out_0_ PRC_u_AT_outMY_ABS_0_)) (= PRC_u_AT_in_0_ PRC_u_AT_inMY_ABS_0_)) (= PRC_u_AT_in_1_ PRC_u_AT_inMY_ABS_1_)) (= PRC_p_A_1_ PRC_p_AMY_ABS_1_)) (= PRC_p_A_0_ PRC_p_AMY_ABS_0_)) (= PRC_u_PA_out_0_ PRC_u_PA_outMY_ABS_0_)) (= PRC_u_PA_out_1_ PRC_u_PA_outMY_ABS_1_)))
(assert
(and (and (= PRC_in_d1_0_ PRC_Filtering__of__pressure_in_d1_0_) (and (= PRC_in_d2_0_ PRC_Filtering__of__pressure_in_d2_0_) (and (and (> PRC_in_d1_0_ (- Inf)) (< PRC_in_d1_0_ Inf)) (and (> PRC_in_d2_0_ (- Inf)) (< PRC_in_d2_0_ Inf))))) (and (= PRC_in_d1_1_ PRC_Filtering__of__pressure_in_d1_1_) (and (= PRC_in_d2_1_ PRC_Filtering__of__pressure_in_d2_1_) (and (and (> PRC_in_d1_1_ (- Inf)) (< PRC_in_d1_1_ Inf)) (and (> PRC_in_d2_1_ (- Inf)) (< PRC_in_d2_1_ Inf)))))))
(assert
(forall ((x double)) (! (iff (isinteger x ) (= x (to_real (to_int x ) ))) :pattern (isinteger x))))
(assert
(forall ((x double)) (! (= (my_abs x ) (if_then_else (< x 0.0) (- x) x)) :pattern (my_abs x))))
(assert 
(< Inf _NaN))
(assert
(< 1000000000000000000000.0 Inf))
(assert
(not (and (and (> Controller.p_hyst 0.0) (and (= Controller.p_hyst 5.0) (= Controller.p_max 200000.0))) (and (and (> PRC_p_A_0_ (- 1000000.0)) (< PRC_p_A_0_ 1000000.0)) (forall ((PRC_Filtering__of__pressure_p_A_filtered_0__primed double)) (implies (and (> PRC_Filtering__of__pressure_p_A_filtered_0__primed (- 1000000.0)) (and (< PRC_Filtering__of__pressure_p_A_filtered_0__primed 1000000.0) (implies (and (= PRC_p_A_0_ PRC_Filtering__of__pressure_in_d1_0_) (= PRC_Filtering__of__pressure_in_d1_0_ PRC_Filtering__of__pressure_in_d2_0_)) (<= (my_abs (- PRC_Filtering__of__pressure_p_A_filtered_0__primed PRC_p_A_0_) ) (* (/ Controller.p_hyst 100.0) (/ Controller.p_max 2.0)))))) (forall ((PRC_Filtering__of__pressure_in_d1_0__primed double)(PRC_Filtering__of__pressure_in_d2_0__primed double)) (implies (and (= PRC_Filtering__of__pressure_in_d1_0__primed PRC_p_A_0_) (= PRC_Filtering__of__pressure_in_d2_0__primed PRC_Filtering__of__pressure_in_d1_0_)) (and (and (> Controller.p_hyst 0.0) (and (= Controller.p_hyst 5.0) (= Controller.p_max 200000.0))) (and (and (> PRC_p_A_1_ (- 1000000.0)) (< PRC_p_A_1_ 1000000.0)) (forall ((PRC_Filtering__of__pressure_p_A_filtered_1__primed double)) (implies (and (> PRC_Filtering__of__pressure_p_A_filtered_1__primed (- 1000000.0)) (and (< PRC_Filtering__of__pressure_p_A_filtered_1__primed 1000000.0) (implies (and (= PRC_p_A_1_ PRC_Filtering__of__pressure_in_d1_1_) (= PRC_Filtering__of__pressure_in_d1_1_ PRC_Filtering__of__pressure_in_d2_1_)) (<= (my_abs (- PRC_Filtering__of__pressure_p_A_filtered_1__primed PRC_p_A_1_) ) (* (/ Controller.p_hyst 100.0) (/ Controller.p_max 2.0)))))) (forall ((PRC_Filtering__of__pressure_in_d1_1__primed double)(PRC_Filtering__of__pressure_in_d2_1__primed double)) (implies (and (= PRC_Filtering__of__pressure_in_d1_1__primed PRC_p_A_1_) (= PRC_Filtering__of__pressure_in_d2_1__primed PRC_Filtering__of__pressure_in_d1_1_)) (and (and (= Controller.Q_max_unit 1.5) (and (> Controller.Q_max_unit 0.0) (and (isinteger Controller.pcCount ) (and (> Controller.pcCount 0.0) (and (= Controller.pcCount 31.0) (and (= Controller.p_max 200000.0) (and (= p_cracking (* 0.9 200000.0)) (< p_cracking Controller.p_max)))))))) (and (and (isinteger PRC_u_AT_in_1_ ) (and (>= PRC_u_AT_in_1_ 0.0) (and (<= PRC_u_AT_in_1_ Controller.pcCount) (and (> PRC_Filtering__of__pressure_p_A_filtered_0__primed (- 1000000.0)) (< PRC_Filtering__of__pressure_p_A_filtered_0__primed 1000000.0))))) (forall ((PRC_Pressure__controller_u_AT_out_primed double)) (implies (and (isinteger PRC_Pressure__controller_u_AT_out_primed ) (and (>= PRC_Pressure__controller_u_AT_out_primed 0.0) (and (<= PRC_Pressure__controller_u_AT_out_primed Controller.pcCount) (and (implies (> PRC_Filtering__of__pressure_p_A_filtered_0__primed Controller.p_max) (= PRC_Pressure__controller_u_AT_out_primed Controller.pcCount)) (and (>= (* PRC_Pressure__controller_u_AT_out_primed Controller.Q_max_unit) (* PRC_u_AT_in_1_ Controller.Q_max_unit)) (implies (< PRC_Filtering__of__pressure_p_A_filtered_0__primed p_cracking) (= PRC_u_AT_in_1_ PRC_Pressure__controller_u_AT_out_primed))))))) (not (and (and (= Controller.p_hyst 5.0) (and (= Controller.Q_max_unit 1.5) (and (> Controller.Q_max_unit 0.0) (and (= Controller.pcCount 31.0) (and (isinteger Controller.pcCount ) (and (> Controller.pcCount 0.0) (and (= Controller.pcCount 31.0) (and (= Controller.p_max 200000.0) (and (= p_cracking (* 0.9 200000.0)) (< p_cracking Controller.p_max)))))))))) (and (and (isinteger PRC_u_AT_inMY_ABS_0_ ) (and (> PRC_p_AMY_ABS_0_ (- 1000000.0)) (and (< PRC_p_AMY_ABS_0_ 1000000.0) (and (>= PRC_u_AT_inMY_ABS_0_ 0.0) (<= PRC_u_AT_inMY_ABS_0_ Controller.pcCount))))) (forall ((PRC_u_AT_outMY_ABS_0__primed double)(PRC_u_PA_outMY_ABS_0__primed double)) (implies (and (isinteger PRC_u_AT_outMY_ABS_0__primed ) (and (>= PRC_u_AT_outMY_ABS_0__primed 0.0) (and (<= PRC_u_AT_outMY_ABS_0__primed Controller.pcCount) (implies (and (= PRC_p_AMY_ABS_0_ PRC_in_d1_0_) (= PRC_in_d1_0_ PRC_in_d2_0_)) (and (implies (> PRC_p_AMY_ABS_0_ (+ Controller.p_max (* (/ Controller.p_hyst 100.0) (/ Controller.p_max 2.0)))) (= PRC_u_AT_outMY_ABS_0__primed Controller.pcCount)) (implies (< PRC_p_AMY_ABS_0_ (- p_cracking (* (/ Controller.p_hyst 100.0) (/ Controller.p_max 2.0)))) (= PRC_u_AT_inMY_ABS_0_ PRC_u_AT_outMY_ABS_0__primed))))))) (forall ((PRC_in_d1_1__primed double)(PRC_in_d2_1__primed double)) (implies (and (= PRC_in_d1_1__primed PRC_p_AMY_ABS_0_) (= PRC_in_d2_1__primed PRC_in_d1_0_)) (and (and (isinteger PRC_u_AT_inMY_ABS_1_ ) (and (> PRC_p_AMY_ABS_1_ (- 1000000.0)) (and (< PRC_p_AMY_ABS_1_ 1000000.0) (and (>= PRC_u_AT_inMY_ABS_1_ 0.0) (<= PRC_u_AT_inMY_ABS_1_ Controller.pcCount))))) (forall ((PRC_u_AT_outMY_ABS_1__primed double)(PRC_u_PA_outMY_ABS_1__primed double)) (implies (and (isinteger PRC_u_AT_outMY_ABS_1__primed ) (and (>= PRC_u_AT_outMY_ABS_1__primed 0.0) (and (<= PRC_u_AT_outMY_ABS_1__primed Controller.pcCount) (implies (and (= PRC_p_AMY_ABS_1_ PRC_in_d1_1__primed) (= PRC_in_d1_1__primed PRC_in_d2_1__primed)) (and (implies (> PRC_p_AMY_ABS_1_ (+ Controller.p_max (* (/ Controller.p_hyst 100.0) (/ Controller.p_max 2.0)))) (= PRC_u_AT_outMY_ABS_1__primed Controller.pcCount)) (implies (< PRC_p_AMY_ABS_1_ (- p_cracking (* (/ Controller.p_hyst 100.0) (/ Controller.p_max 2.0)))) (= PRC_u_AT_inMY_ABS_1_ PRC_u_AT_outMY_ABS_1__primed))))))) (forall ((PRC_in_d1_0__primed double)(PRC_in_d2_0__primed double)) (implies (and (= PRC_in_d1_0__primed PRC_p_AMY_ABS_1_) (= PRC_in_d2_0__primed PRC_in_d1_1__primed)) (not (and (and (and (and (and (and (and (and (= PRC_Pressure__controller_u_AT_out_primed PRC_u_AT_outMY_ABS_1__primed) (= PRC_Pressure__controller_u_AT_out_primed PRC_u_AT_outMY_ABS_0__primed)) (= PRC_u_AT_in_0_ PRC_u_AT_inMY_ABS_0_)) (= PRC_u_AT_in_1_ PRC_u_AT_inMY_ABS_1_)) (= PRC_p_A_1_ PRC_p_AMY_ABS_1_)) (= PRC_p_A_0_ PRC_p_AMY_ABS_0_)) (= PRC_u_PA_in_1_ PRC_u_PA_outMY_ABS_0__primed)) (= PRC_u_PA_in_1_ PRC_u_PA_outMY_ABS_1__primed)) (and (and (= PRC_in_d1_0__primed PRC_Filtering__of__pressure_in_d1_0__primed) (and (= PRC_in_d2_0__primed PRC_Filtering__of__pressure_in_d2_0__primed) (and (and (> PRC_in_d1_0__primed (- Inf)) (< PRC_in_d1_0__primed Inf)) (and (> PRC_in_d2_0__primed (- Inf)) (< PRC_in_d2_0__primed Inf))))) (and (= PRC_in_d1_1__primed PRC_Filtering__of__pressure_in_d1_1__primed) (and (= PRC_in_d2_1__primed PRC_Filtering__of__pressure_in_d2_1__primed) (and (and (> PRC_in_d1_1__primed (- Inf)) (< PRC_in_d1_1__primed Inf)) (and (> PRC_in_d2_1__primed (- Inf)) (< PRC_in_d2_1__primed Inf))))))))))))))))))))))))))))))))))))))

(check-sat)
;; (get-model)